T:Type, eq:EqDecider(T), es:event_system{i:l}, x:Id, e:{e:es-E(es)| es-dtype(es; loc(e); x; T)} ,
t:rationals, e':es-E(es), v:T.
(x unchanged-for t @ e)
 @e'(xv)
 es-locl(es; e'; e)
 qle((es-time(es; e') + t); es-time(es; e)) 

latex

Definitions

P  Q, P  Q, True, T, es-dtype(es; i; x; T), A, prop{i:l}, A c B, x:A. B(x), P  Q, e<e'.P(e), es-locl(es; e; e'), t  T, P  Q, x:A. B(x), guard(T), SqStable(P), (x unchanged-for t @ e), False, @e(xv), subtype(S; T), !hyp_hide(x)  {FDLNOr12445}

Lemmas

mon ident q, qinverse q, qadd comm q, qadd ac 1 q, true wf, squash wf, qadd preserves qle, iff transitivity, int inc rationals, qmul wf, qle wf, es-time wf, qadd wf, qle transitivity qorder, es-causl weakening, es-causle weakening locl, sq stable subtype rel, decidable assert, es-isconst wf, assert wf, sq stable from decidable, es-le-last-change, last-change wf, es-causle-time, es-when wf, es-vartype wf, es-after wf, not wf, es-causl wf, assert-changed, deq wf, event system wf, Id wf, es-loc wf, es-dtype wf, rationals wf, es-E wf, unchanged-for wf, es-change-to wf, es-locl wf